f2(a, h1(x)) -> f2(g1(x), h1(x))
h1(g1(x)) -> h1(a)
g1(h1(x)) -> g1(x)
h1(h1(x)) -> x
↳ QTRS
↳ DependencyPairsProof
f2(a, h1(x)) -> f2(g1(x), h1(x))
h1(g1(x)) -> h1(a)
g1(h1(x)) -> g1(x)
h1(h1(x)) -> x
G1(h1(x)) -> G1(x)
F2(a, h1(x)) -> G1(x)
H1(g1(x)) -> H1(a)
F2(a, h1(x)) -> F2(g1(x), h1(x))
f2(a, h1(x)) -> f2(g1(x), h1(x))
h1(g1(x)) -> h1(a)
g1(h1(x)) -> g1(x)
h1(h1(x)) -> x
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
G1(h1(x)) -> G1(x)
F2(a, h1(x)) -> G1(x)
H1(g1(x)) -> H1(a)
F2(a, h1(x)) -> F2(g1(x), h1(x))
f2(a, h1(x)) -> f2(g1(x), h1(x))
h1(g1(x)) -> h1(a)
g1(h1(x)) -> g1(x)
h1(h1(x)) -> x
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
G1(h1(x)) -> G1(x)
f2(a, h1(x)) -> f2(g1(x), h1(x))
h1(g1(x)) -> h1(a)
g1(h1(x)) -> g1(x)
h1(h1(x)) -> x
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G1(h1(x)) -> G1(x)
POL(G1(x1)) = 2·x1
POL(h1(x1)) = 1 + 2·x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
f2(a, h1(x)) -> f2(g1(x), h1(x))
h1(g1(x)) -> h1(a)
g1(h1(x)) -> g1(x)
h1(h1(x)) -> x
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
F2(a, h1(x)) -> F2(g1(x), h1(x))
f2(a, h1(x)) -> f2(g1(x), h1(x))
h1(g1(x)) -> h1(a)
g1(h1(x)) -> g1(x)
h1(h1(x)) -> x
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F2(a, h1(x)) -> F2(g1(x), h1(x))
POL(F2(x1, x2)) = 2·x1
POL(a) = 2
POL(g1(x1)) = 1
POL(h1(x1)) = 0
g1(h1(x)) -> g1(x)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
f2(a, h1(x)) -> f2(g1(x), h1(x))
h1(g1(x)) -> h1(a)
g1(h1(x)) -> g1(x)
h1(h1(x)) -> x